p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))), s, k:.
(n:, i:{0..n}. f(i) < f(n))
 (n:.
 E(f(n);X(n)) = 0   & E(f(n);(x.x * x) o X(n)) = s & E(f(n);(x.(x * x) * x * x) o X(n)) = k)
 (n:, i:{0..n}. rv-disjoint(p;f(n);X(i);X(n)))
 (B:
 ((n:.
 (E(f(n);rv-partial-sum(n;k.if (k = 0)
 (then 0
 (else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X(i))
 (fi ))  B)) 

latex

Definitions

, x:A. B(x), , , x:A  B(x), A  B, , s = t, EquivRel(T;x,y.E(x;y)), P  Q, False, A, P & Q, A  B, i  j < k, {x:A| B(x)} , {i..j}, x:AB(x), tt, qeq(r;s), , x,y. t(x;y), x,y:A//B(x;y), Type, FinProbSpace, Top, type List, f(a), <a, b>, True, T, RandomVariable(p;n), Void, x:A.B(x), S  T, P  Q, t  ...$L, rv-disjoint(p;n;X;Y), a  b, r  s, s ~ t, {T}, SQType(T), (r/s), if b then t else f fi , x.A(x), x. t(x), rv-partial-sum(n;i.X(i)), q*X, (x.F(x)) o X, b, b, rv-const(a), (i = j), Unit, left + right, E(n;F), x:A. B(x), #$n, r * s, ||as||, , t  T, x(s), a < b, a  j < b. E(j), P  Q, P  Q, isint(z;a;b), case b of inl(x) => s(x) | inr(y) => t(y), Outcome, Mon, Group{i}, AbGrp, <+>, , x f y, a  b, -n, r < s, a < b, a <p b, DSet, QOSet, POSet{i}, LOSet, AbMon, OMon, goset, a < b, X  Y, Dec(P), r + s

Lemmas

qle-iff, qmul preserves qless, qmul-qdiv-cancel, qmul one qrng, qle weakening lt qorder, int seg properties, qmul over plus qrng, qadd wf, mon ident q, decidable equal rationals, qsum-reciprocal-squares-bound, sum unroll lo q, sum unroll base q, prod sum l q, decidable int equal, qsum wf, qmul com, qmul assoc, q-square-non-neg, expectation-non-neg, qmul preserves qle, qmul zero qrng, qmul-qdiv-cancel2, qmul-positive, qless wf, qless-int, qle functionality wrt implies, qmul functionality wrt qle, expectation-rv-scale, qmul-qdiv, nat properties, qmul assoc qrng, qmul comm qrng, qmul ac 1 qrng, or functionality wrt iff, p-outcome wf, expectation-monotone-in-first, expectation-rv-const, non-neg-qmul, qle weakening eq qorder, qsum-qle, qmul-zero, expectation-qsum, rv-disjoint wf, slln-lemma1, qle wf, expectation wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, rv-const wf, bnot wf, not wf, assert wf, rv-compose wf, rv-scale wf, rv-partial-sum wf, qdiv wf, int inc rationals, int-rational, qmul wf, int-eq-in-rationals, top wf, random-variable wf, finite-prob-space wf, subtype rel function, squash wf, true wf, le wf, length wf nat, int seg wf, nat wf, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, rationals wf